Definitions | Dec(P), x(s), ES, False, x:A. B(x), A & B, e e' , x(s1,s2), A, ( x L.P(x)), e@i.P(e),  x. t(x), True, E, Id, loc(e), x L. P(x), (x l), P  Q, P & Q, P  Q, {T}, P  Q, Prop, x:A. B(x), t T, P Q, {i..j }, i j < k, A B, l[i], i j, i< j, hd(l), i j, ||as||, (e <loc e'), Trans x,y:T. E(x;y) |